es:ES, A:Type, l:IdLnk, tg:Id, ds:x:Id fp Type,
conds:k:Knd fp V:Type  (State(ds)V(A + Top)).
sender-glues-triggers-p(es; A; l; tg; ds; conds)  triggers-glued-p(es; A; l; tg; ds; conds) 

latex

Definitions	t  T, P  Q, x:A. B(x), Top, E(X),
Lemmas	es-valtype wf, es-in-port wf, es-E-interface wf, es-sender wf